Nuprl Lemma : comb_for_swap_wf
4,23
postcript
pdf
(
T
,
L
,
i
,
j
,
z
. swap(
L
;
i
;
j
))
T
:Type
L
:(
T
List)
||
L
||
||
L
||
True
(
T
List)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
True
,
T
Lemmas
swap
wf
,
squash
wf
,
true
wf
,
int
seg
wf
,
length
wf1
origin
T,L,i,j,z. swap(L;i;j)) 
T:Type
L:(T List)
||L||||L||
True(T List) T,L,i,j,z. swap(L;i;j)) T:TypeL:(T List)||L||||L||True(T List) T
x:A. B(x)
}T